|
In finite-state verification, model checkers examine finite-state machines representing concurrent software systems looking for errors in design. Errors are defined as violations of requirements expressed as properties of the system. In the event that the finite-state machine fails to satisfy the property, a model checker is in some cases capable of producing a counterexample – an execution of the system demonstrating how the error occurs. Property specifications are often written as Linear Temporal Logic (LTL) expressions. Once a requirement is expressed as an LTL formula, a model checker can automatically verify this property against the model. ==Example== One example of such a system requirement: ''Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice''.〔M. Dwyer, G. Avruin, J. Corbett, Y. Hu, "Patterns in Property Specification for Finite-State Verification." In M. Ardis, editor, ''Proceedings of the Second Workshop on Formal Methods in Software Practice'', pages 7–15, March 1998.〕 The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula: : 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Temporal logic in finite-state verification」の詳細全文を読む スポンサード リンク
|